Hardware Memory Models
Introduction: A Fairy Tale, Ending
御伽噺の時代
何もしなくてもコンパイラとプロセッサーが次世代になればプログラムは早くなった
最適化がただしいかのテストも簡単だった
正しい最適化は正しいプログラムの振る舞いを変えない
プロセッサを増やすことが始まった
OSはハードウェアのparallelismをthreadとしてプログラマに晒すようになった
言語デザイナ、コンパイラ開発者、そしてプログラマにとって新しい問題
シングルスレッドの正しい最適化はマルチスレッドプログラムの振る舞いを変えるようになった
最適化か、プログラムか、どちらかが間違っている(invalid)
どちらなのかどうやったらわかるのだろうか?
プログラム例
0を出力することがあるか?
depends on hardware & compiler.
direct line-to-line translation
x86→常に1
ARM/POWER→0かも
コンパイラ最適化がある
0
無限ループ
「場合による」は嬉しくないのでメモリーモデルが必要
ハードウェア設計者
コンパイラ開発者
アプリケーションプログラマ
主たる問題であるメモリ上のデータの「可視性」と「一貫性」に関する契約のことをメモリーモデルと呼ぶ
初めはメモリーモデルにコンパイラは関係なかったが、高級言語が使われるようになったことでコンパイラも「メモリモデル」の登場人物になった
この論文は、次のテーマを扱う
ハードウェアメモリモデル
プログラム言語メモリモデル
Goのメモリモデルに行いたいかもしれない変更
このポストでは、「アセンブリ言語でマルチプロセッサコンピュータのプログラムを書いている」とする
プログラマはどんな保証をハードウェアにしてほしいか
コンピュータ科学者は色々考えてきた
Sequential Consistency
逐次一貫性? wikipedia
全てのプロセッサーはあるシーケンシャルな順序で実行される
各プロセッサ内の処理はプログラムに書かれた順序で実行される
今日では逐次一貫性はハードウェアだけでなくプログラム言語にも適用される
「逐次一貫性を持つプログラム言語」のような感じ?
ここわからない
理想的なモデルとされる(プログラマにとって)
このパラグラフはよくわからない
リトマステストを考える(共有メモリ上の変数の読み出しについて)
リトマステストはYes/Noで答えられる問題なので、メモリーモデルを区別することに使える
しばしばリトマステストの答えは驚くべきものである
逐次一貫なモデルにおいて(r1, r2) = (1, 0)は起きえない
逐次一貫性を理解する良いメンタルモデル=全てのプロセッサーが同一の共有メモリに直接繋がっているモデル
キャッシュが存在しない
読み込み、書き込み要求は直接共有メモリにいく
共有メモリは同時に複数プロセッサからは使えないという仮定もある→シーケンシャルコンシステンシーになる
このモデルで考えれば逐次一貫性のある実行は理解できる!!
逐次一貫性を放棄するとハードウェアは早くなるので、色々な方法で現代のハードウェアは逐次一貫性を逸脱している
具体例二つをモデル化して説明する
x86
ARM/POWER families
x86 Total Store Order (x86-TSO)
全てのプロセッサは共有メモリに繋がっているが、書き込みキューがプロセッサごとにあるモデル
プロセッサからの読み込みは共有メモリよりも先に書き込みキューを読みにいく!
他のプロセッサの書き込みキューは見られない
しかし、全てのプロセッサは、全ての書き込みが共有メモリに到達する順序については同意する(同じ順序を観測する)
→Total Store Order(TSO)と呼ばれる理由
共有メモリの到達した書き込みは全てのプロセッサから観測できる
先程のリトマステストではTSOとSCは区別できない
他のリトマステストで区別できる
barrier命令で逐次一貫性のある振る舞いを特定の場所で強制する手段が与えられている
なぜTotal Store Orderと呼ばれるか?
書き込みが共有メモリに到達すれば、全てのプロセッサはその値がそこにあるということだけではなく、その値が他の書き込みと比べて早くきたか遅くきたかについても合意することができる
全順序のこと
「共有メモリに到達した全ての書き込みの集合」=全順序集合
全てのw1, w2に対して、 w1 < w2, w1 = w2, w1 > w2のいずれかが成り立つ
IRIWリトマステスト
The Path to x86-TSO
クリーンなモデルに見えるけど紆余曲折あった。最初のマニュアルにはメモリモデルなんてほとんど書かれてなかった
引用されている段落はよくわからない、lockって共有メモリに対するロック?
最初の明確なメモリモデルは2007に定義された?
AMDもモデルを定義した。Total lock order + causal consistency(TLO + CO)
weaker than TSO
TLO+COのバリアは不十分で、SCを回復する手段がなかった
As strong as required but no strongerはとても難しいゴールで、アーキテクトはすごく苦労してTSOに辿り着いた
ARM/POWER Relaxed Memory Model
ARMとPOWERは同じメモリモデルを保証するが、これはx86-TSOよりかなり「弱い」
それぞれのプロセッサが固有のメモリから読み書きする
それぞれの書き込みは独立に他のプロセッサのメモリに伝播する
その際順番が入れ替わっても良い
Total Store Orderなし
図に書かれていないけど、プロセッサは読み出しをその結果が必要となるまで遅らせることができる(別な書き込みの時まで)
ARM/POWERモデルはIRIWに対してyesを返す
ARM/POWERは何が起きないことを保証してくれるのか?
Coherenceテスト
単一のメモリについてのTotal Orderのこと
「どの書き込みがどの書き込みを上書きするか」については全てのプロセッサが合意できる
コヒーレンスと呼ばれている性質
もしコヒーレンスがなかったら、ある変数の最終的な値すら一つに決まらないし、2つの値を行ったり来たりすることすらありうる←なぜ?
そんなハードウェアをプログラムするのは難しい
複雑な点は省いたよ
ARMv8というのがあってmulticopy atomicとかいう性質を保証したより強いモデルを提供するけど、ここでは触れない
2つの補足
まじ難しいから全部理解するの無理
ハードウェアとモデルの乖離があると簡単に強いモデルに暗黙的に依存したプログラムを書いてしまう、辛い
Weak Ordering and Data-Race-Free Sequential Consistency
ハードウェアの詳細(メモリモデル)を考えてプログラムするのはとても辛い
簡単なルールに従えば、逐次一貫性のあるインタリービングが保証される、ってなってると嬉しい
あくまでまだアセンブリのインタリービングの話をしている
1990の論文で”Weakly Ordered”が定義された
同期モデル=いつどのように同期が行われなければならないか、のルールの集まり
「ハードウェアがある同期モデルMについてWeakly orderedである」とは、「同期モデルに従う全てのソフトウェアに対して、逐次一貫性をもって振る舞うこと」をいう
Adve&Hill論文ではdata-race-free(DRF)という同期モデルが提案された
同期オペレーションをハードウェアが提供する前提
sync opの間ではwrite/readはreorderできる
reorder(順序の入れ替え)に対するbarrierになる
プログラムは次の時に、data-race-freeであるという:
全ての理想化された逐次一貫性のある実行において、
別スレッドからの同一のメモリ位置に対するどのような2つのメモリアクセス(read/write)も、次のいずれかを満たす
2つともreadである
syncによって分断されることで、どちらかがどちらかよりも先に起こるようになっている
↓こういうこと?
r1, r2, sync →OK
r1, sync, r2 →OK
r1, sync, w1→OK
r1, w1, sync→だめ
具体例
あらゆるレースは少なくとも1つの書き込みが関わる
weak ordering = ソフトウェアとハードウェアの契約
ある種の最低限の要求を満たすならばそのハードウェアはDRFについてweakly orderedであることを証明した
ハードウェアがDRFを満たすプログラムに対して逐次一貫性を持って振る舞うという性質は、DRF-SCとも呼ばれる
要するに、アセンブリ言語において適切にsyncをすれば、SCが保証されるということ
x86, ARM, POWERはDRF-SCを満たす
DRF-SCはハードウェア設計者とソフトウェア開発者の両方にとって明確な指針を与えた
しかし、高水準言語に対するメモリモデルはこれほど簡潔な答えはない